Debugging large scale systems has been attempted using fully-automated systems, such as systems that check the behavior of a system against an ideal model of the system. However, while some problems may be identified using automated systems, fully modeling the logic of a complex protocol requires a complex model, which can increase the probability of bugs in the model. Complex models may also have difficulty with boundaries between simulated code modules, ossification of legacy code, privacy or trade secret issues (e.g., when the software developer and the debugger belong to different institutions or organizations), and scaling issues. Fully automated models often detect problems without determining the root cause of the problem or how the problem may be repaired. Additionally, fully automated models tend to have difficulty identifying logical or semantic errors, such as may exist in source code.